The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0, cons(X, Z)) → X
first(0, Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0, cons(X, Z)) → quote(X)
first1(0, Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01) → 0
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
quote1(n__cons(X, Z)) →⁺ cons1(quote(activate(X)), quote1(Z))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [Z / n__cons(X, Z)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
sel, activate, sel1, quote, first1, quote1, unquote, unquote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(8) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
unquote, sel, activate, sel1, quote, first1, quote1, unquote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1
unquote < unquote1

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

Induction Base:
unquote(gen_01':s15_3(+(1, 0)))

Induction Step:
unquote(gen_01':s15_3(+(1, +(n8_3, 1)))) →_R^Ω(1)
s(unquote(gen_01':s15_3(+(1, n8_3)))) →_IH
s(*7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
unquote1, sel, activate, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Induction Base:
unquote1(gen_nil1:cons16_3(0))

Induction Step:
unquote1(gen_nil1:cons16_3(+(n1023_3, 1))) →_R^Ω(1)
fcons(unquote(01'), unquote1(gen_nil1:cons16_3(n1023_3))) →_R^Ω(1)
fcons(0', unquote1(gen_nil1:cons16_3(n1023_3))) →_R^Ω(1)
fcons(n__0, unquote1(gen_nil1:cons16_3(n1023_3))) →_IH
fcons(n__0, *7_3)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(13) Complex Obligation (BEST)

(14) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
activate, sel, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol activate.

(16) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
sel, sel1, quote, first1, quote1

They will be analysed ascendingly in the following order:
sel = activate
activate < sel1
activate < quote
activate < first1
activate < quote1
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol sel.

(18) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
quote, sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol quote.

(20) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
sel1, first1, quote1

They will be analysed ascendingly in the following order:
sel1 = quote
quote < first1
quote < quote1
first1 < quote1

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol sel1.

(22) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
first1, quote1

They will be analysed ascendingly in the following order:
first1 < quote1

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol first1.

(24) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

The following defined symbols remain to be analysed:
quote1

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol quote1.

(26) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

(28) BOUNDS(n^1, INF)

(29) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)
unquote1(gen_nil1:cons16_3(n1023_3)) → *7_3, rt ∈ Ω(n1023₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

(31) BOUNDS(n^1, INF)

(32) Obligation:

TRS:
Rules:
sel(s(X), cons(Y, Z)) → sel(X, activate(Z))
sel(0', cons(X, Z)) → X
first(0', Z) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
from(X) → cons(X, n__from(s(X)))
sel1(s(X), cons(Y, Z)) → sel1(X, activate(Z))
sel1(0', cons(X, Z)) → quote(X)
first1(0', Z) → nil1
first1(s(X), cons(Y, Z)) → cons1(quote(Y), first1(X, activate(Z)))
quote(n__0) → 01'
quote1(n__cons(X, Z)) → cons1(quote(activate(X)), quote1(activate(Z)))
quote1(n__nil) → nil1
quote(n__s(X)) → s1(quote(activate(X)))
quote(n__sel(X, Z)) → sel1(activate(X), activate(Z))
quote1(n__first(X, Z)) → first1(activate(X), activate(Z))
unquote(01') → 0'
unquote(s1(X)) → s(unquote(X))
unquote1(nil1) → nil
unquote1(cons1(X, Z)) → fcons(unquote(X), unquote1(Z))
fcons(X, Z) → cons(X, Z)
first(X1, X2) → n__first(X1, X2)
from(X) → n__from(X)
0' → n__0
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
s(X) → n__s(X)
sel(X1, X2) → n__sel(X1, X2)
activate(n__first(X1, X2)) → first(X1, X2)
activate(n__from(X)) → from(X)
activate(n__0) → 0'
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__s(X)) → s(X)
activate(n__sel(X1, X2)) → sel(X1, X2)
activate(X) → X

Types:
sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
activate :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
0' :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__first :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__from :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
sel1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
quote :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → 01':s1
first1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
nil1 :: nil1:cons1
cons1 :: 01':s1 → nil1:cons1 → nil1:cons1
n__0 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
01' :: 01':s1
quote1 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → nil1:cons1
n__cons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__nil :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
n__s :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
s1 :: 01':s1 → 01':s1
n__sel :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote :: 01':s1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
unquote1 :: nil1:cons1 → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
fcons :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel1_3 :: n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
hole_01':s12_3 :: 01':s1
hole_nil1:cons13_3 :: nil1:cons1
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3 :: Nat → n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel
gen_01':s15_3 :: Nat → 01':s1
gen_nil1:cons16_3 :: Nat → nil1:cons1

Lemmas:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

Generator Equations:
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(0) ⇔ n__0
gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(+(x, 1)) ⇔ n__first(n__0, gen_n__first:n__from:n__0:n__cons:n__nil:n__s:n__sel4_3(x))
gen_01':s15_3(0) ⇔ 01'
gen_01':s15_3(+(x, 1)) ⇔ s1(gen_01':s15_3(x))
gen_nil1:cons16_3(0) ⇔ nil1
gen_nil1:cons16_3(+(x, 1)) ⇔ cons1(01', gen_nil1:cons16_3(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
unquote(gen_01':s15_3(+(1, n8_3))) → *7_3, rt ∈ Ω(n8₃)

(34) BOUNDS(n^1, INF)